A:MsgA, k:Knd. ma-has-sends(A;k)  Prop 

latex

Definitions	Knd, t  T, IdLnk, x:A. B(x), x. t(x), 1of(t), map(f;as), KindDeq, deq-member(eq;x;L), b, Prop, a:A fp B(a), ma-has-sends(M;k), MsgA
Lemmas	msga wf, assert wf, deq-member wf, Kind-deq wf, map wf, pi1 wf, IdLnk wf, Knd wf